The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0) → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
fold(t, x, 0) → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Rewrite Strategy: INNERMOST

(1) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(2) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0', c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

S is empty.
Rewrite Strategy: INNERMOST

(3) SlicingProof (LOWER BOUND(ID) transformation)

Sliced the following arguments:
triple/0

(4) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(b, c), C) → triple(b, s(c))
f'(triple(b, c), B) → f(triple(b, c), A)
f'(triple(b, c), A) → f''(foldB(triple(0', c), b))
f''(triple(b, c)) → foldC(triple(b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

S is empty.
Rewrite Strategy: INNERMOST

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(6) Obligation:

Innermost TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(b, c), C) → triple(b, s(c))
f'(triple(b, c), B) → f(triple(b, c), A)
f'(triple(b, c), A) → f''(foldB(triple(0', c), b))
f''(triple(b, c)) → foldC(triple(b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

(7) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
foldB, f, foldC, f', f'', fold

They will be analysed ascendingly in the following order:
foldB = f
foldB = foldC
foldB = f'
foldB = f''
f = foldC
f = f'
f = f''
f < fold
foldC = f'
foldC = f''
f' = f''

(8) Obligation:

Innermost TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(b, c), C) → triple(b, s(c))
f'(triple(b, c), B) → f(triple(b, c), A)
f'(triple(b, c), A) → f''(foldB(triple(0', c), b))
f''(triple(b, c)) → foldC(triple(b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

The following defined symbols remain to be analysed:
f, foldB, foldC, f', f'', fold

They will be analysed ascendingly in the following order:
foldB = f
foldB = foldC
foldB = f'
foldB = f''
f = foldC
f = f'
f = f''
f < fold
foldC = f'
foldC = f''
f' = f''

(9) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol f.

(10) Obligation:

Innermost TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(b, c), C) → triple(b, s(c))
f'(triple(b, c), B) → f(triple(b, c), A)
f'(triple(b, c), A) → f''(foldB(triple(0', c), b))
f''(triple(b, c)) → foldC(triple(b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

The following defined symbols remain to be analysed:
f', foldB, foldC, f'', fold

They will be analysed ascendingly in the following order:
foldB = f
foldB = foldC
foldB = f'
foldB = f''
f = foldC
f = f'
f = f''
f < fold
foldC = f'
foldC = f''
f' = f''

(11) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol f'.

(12) Obligation:

Innermost TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(b, c), C) → triple(b, s(c))
f'(triple(b, c), B) → f(triple(b, c), A)
f'(triple(b, c), A) → f''(foldB(triple(0', c), b))
f''(triple(b, c)) → foldC(triple(b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

The following defined symbols remain to be analysed:
f'', foldB, foldC, fold

They will be analysed ascendingly in the following order:
foldB = f
foldB = foldC
foldB = f'
foldB = f''
f = foldC
f = f'
f = f''
f < fold
foldC = f'
foldC = f''
f' = f''

(13) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol f''.

(14) Obligation:

Innermost TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(b, c), C) → triple(b, s(c))
f'(triple(b, c), B) → f(triple(b, c), A)
f'(triple(b, c), A) → f''(foldB(triple(0', c), b))
f''(triple(b, c)) → foldC(triple(b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

The following defined symbols remain to be analysed:
foldC, foldB, fold

They will be analysed ascendingly in the following order:
foldB = f
foldB = foldC
foldB = f'
foldB = f''
f = foldC
f = f'
f = f''
f < fold
foldC = f'
foldC = f''
f' = f''

(15) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
foldC(triple(0', 0'), gen_0':s4_0(n143_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n143₀)

Induction Base:
foldC(triple(0', 0'), gen_0':s4_0(0)) →_R^Ω(1)
triple(0', 0')

Induction Step:
foldC(triple(0', 0'), gen_0':s4_0(+(n143_0, 1))) →_R^Ω(1)
f(foldC(triple(0', 0'), gen_0':s4_0(n143_0)), C) →_IH
f(triple(gen_0':s4_0(0), gen_0':s4_0(0)), C) →_R^Ω(1)
f'(triple(gen_0':s4_0(0), gen_0':s4_0(0)), g(C)) →_R^Ω(1)
f'(triple(gen_0':s4_0(0), gen_0':s4_0(0)), A) →_R^Ω(1)
f''(foldB(triple(0', gen_0':s4_0(0)), gen_0':s4_0(0))) →_R^Ω(1)
f''(triple(0', gen_0':s4_0(0))) →_R^Ω(1)
foldC(triple(0', 0'), gen_0':s4_0(0)) →_R^Ω(1)
triple(0', 0')

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(16) Complex Obligation (BEST)

(17) Obligation:

Innermost TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(b, c), C) → triple(b, s(c))
f'(triple(b, c), B) → f(triple(b, c), A)
f'(triple(b, c), A) → f''(foldB(triple(0', c), b))
f''(triple(b, c)) → foldC(triple(b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Lemmas:
foldC(triple(0', 0'), gen_0':s4_0(n143_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n143₀)

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

The following defined symbols remain to be analysed:
foldB, f, f', f'', fold

They will be analysed ascendingly in the following order:
foldB = f
foldB = foldC
foldB = f'
foldB = f''
f = foldC
f = f'
f = f''
f < fold
foldC = f'
foldC = f''
f' = f''

(18) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
foldB(triple(0', 0'), gen_0':s4_0(n2097_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n2097₀)

Induction Base:
foldB(triple(0', 0'), gen_0':s4_0(0)) →_R^Ω(1)
triple(0', 0')

Induction Step:
foldB(triple(0', 0'), gen_0':s4_0(+(n2097_0, 1))) →_R^Ω(1)
f(foldB(triple(0', 0'), gen_0':s4_0(n2097_0)), B) →_IH
f(triple(gen_0':s4_0(0), gen_0':s4_0(0)), B) →_R^Ω(1)
f'(triple(gen_0':s4_0(0), gen_0':s4_0(0)), g(B)) →_R^Ω(1)
f'(triple(gen_0':s4_0(0), gen_0':s4_0(0)), A) →_R^Ω(1)
f''(foldB(triple(0', gen_0':s4_0(0)), gen_0':s4_0(0))) →_R^Ω(1)
f''(triple(0', gen_0':s4_0(0))) →_R^Ω(1)
foldC(triple(0', 0'), gen_0':s4_0(0)) →_L^Ω(1)
triple(gen_0':s4_0(0), gen_0':s4_0(0))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(19) Complex Obligation (BEST)

(20) Obligation:

Innermost TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(b, c), C) → triple(b, s(c))
f'(triple(b, c), B) → f(triple(b, c), A)
f'(triple(b, c), A) → f''(foldB(triple(0', c), b))
f''(triple(b, c)) → foldC(triple(b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Lemmas:
foldC(triple(0', 0'), gen_0':s4_0(n143_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n143₀)
foldB(triple(0', 0'), gen_0':s4_0(n2097_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n2097₀)

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

The following defined symbols remain to be analysed:
f, foldC, f', f'', fold

They will be analysed ascendingly in the following order:
foldB = f
foldB = foldC
foldB = f'
foldB = f''
f = foldC
f = f'
f = f''
f < fold
foldC = f'
foldC = f''
f' = f''

(21) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol f.

(22) Obligation:

Innermost TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(b, c), C) → triple(b, s(c))
f'(triple(b, c), B) → f(triple(b, c), A)
f'(triple(b, c), A) → f''(foldB(triple(0', c), b))
f''(triple(b, c)) → foldC(triple(b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Lemmas:
foldC(triple(0', 0'), gen_0':s4_0(n143_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n143₀)
foldB(triple(0', 0'), gen_0':s4_0(n2097_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n2097₀)

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

The following defined symbols remain to be analysed:
f', foldC, f'', fold

They will be analysed ascendingly in the following order:
foldB = f
foldB = foldC
foldB = f'
foldB = f''
f = foldC
f = f'
f = f''
f < fold
foldC = f'
foldC = f''
f' = f''

(23) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol f'.

(24) Obligation:

Innermost TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(b, c), C) → triple(b, s(c))
f'(triple(b, c), B) → f(triple(b, c), A)
f'(triple(b, c), A) → f''(foldB(triple(0', c), b))
f''(triple(b, c)) → foldC(triple(b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Lemmas:
foldC(triple(0', 0'), gen_0':s4_0(n143_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n143₀)
foldB(triple(0', 0'), gen_0':s4_0(n2097_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n2097₀)

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

The following defined symbols remain to be analysed:
f'', foldC, fold

They will be analysed ascendingly in the following order:
foldB = f
foldB = foldC
foldB = f'
foldB = f''
f = foldC
f = f'
f = f''
f < fold
foldC = f'
foldC = f''
f' = f''

(25) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol f''.

(26) Obligation:

Innermost TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(b, c), C) → triple(b, s(c))
f'(triple(b, c), B) → f(triple(b, c), A)
f'(triple(b, c), A) → f''(foldB(triple(0', c), b))
f''(triple(b, c)) → foldC(triple(b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Lemmas:
foldC(triple(0', 0'), gen_0':s4_0(n143_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n143₀)
foldB(triple(0', 0'), gen_0':s4_0(n2097_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n2097₀)

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

The following defined symbols remain to be analysed:
foldC, fold

They will be analysed ascendingly in the following order:
foldB = f
foldB = foldC
foldB = f'
foldB = f''
f = foldC
f = f'
f = f''
f < fold
foldC = f'
foldC = f''
f' = f''

(27) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
foldC(triple(0', 0'), gen_0':s4_0(n4174_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n4174₀)

Induction Base:
foldC(triple(0', 0'), gen_0':s4_0(0)) →_R^Ω(1)
triple(0', 0')

Induction Step:
foldC(triple(0', 0'), gen_0':s4_0(+(n4174_0, 1))) →_R^Ω(1)
f(foldC(triple(0', 0'), gen_0':s4_0(n4174_0)), C) →_IH
f(triple(gen_0':s4_0(0), gen_0':s4_0(0)), C) →_R^Ω(1)
f'(triple(gen_0':s4_0(0), gen_0':s4_0(0)), g(C)) →_R^Ω(1)
f'(triple(gen_0':s4_0(0), gen_0':s4_0(0)), A) →_R^Ω(1)
f''(foldB(triple(0', gen_0':s4_0(0)), gen_0':s4_0(0))) →_L^Ω(1)
f''(triple(gen_0':s4_0(0), gen_0':s4_0(0))) →_R^Ω(1)
foldC(triple(gen_0':s4_0(0), 0'), gen_0':s4_0(0)) →_R^Ω(1)
triple(gen_0':s4_0(0), 0')

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(28) Complex Obligation (BEST)

(29) Obligation:

Innermost TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(b, c), C) → triple(b, s(c))
f'(triple(b, c), B) → f(triple(b, c), A)
f'(triple(b, c), A) → f''(foldB(triple(0', c), b))
f''(triple(b, c)) → foldC(triple(b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Lemmas:
foldC(triple(0', 0'), gen_0':s4_0(n4174_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n4174₀)
foldB(triple(0', 0'), gen_0':s4_0(n2097_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n2097₀)

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

The following defined symbols remain to be analysed:
fold

(30) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
fold(triple(0', 0'), A, gen_0':s4_0(n6349_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n6349₀)

Induction Base:
fold(triple(0', 0'), A, gen_0':s4_0(0)) →_R^Ω(1)
triple(0', 0')

Induction Step:
fold(triple(0', 0'), A, gen_0':s4_0(+(n6349_0, 1))) →_R^Ω(1)
f(fold(triple(0', 0'), A, gen_0':s4_0(n6349_0)), A) →_IH
f(triple(gen_0':s4_0(0), gen_0':s4_0(0)), A) →_R^Ω(1)
f'(triple(gen_0':s4_0(0), gen_0':s4_0(0)), g(A)) →_R^Ω(1)
f'(triple(gen_0':s4_0(0), gen_0':s4_0(0)), A) →_R^Ω(1)
f''(foldB(triple(0', gen_0':s4_0(0)), gen_0':s4_0(0))) →_L^Ω(1)
f''(triple(gen_0':s4_0(0), gen_0':s4_0(0))) →_R^Ω(1)
foldC(triple(gen_0':s4_0(0), 0'), gen_0':s4_0(0)) →_L^Ω(1)
triple(gen_0':s4_0(0), gen_0':s4_0(0))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(31) Complex Obligation (BEST)

(32) Obligation:

Innermost TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(b, c), C) → triple(b, s(c))
f'(triple(b, c), B) → f(triple(b, c), A)
f'(triple(b, c), A) → f''(foldB(triple(0', c), b))
f''(triple(b, c)) → foldC(triple(b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Lemmas:
foldC(triple(0', 0'), gen_0':s4_0(n4174_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n4174₀)
foldB(triple(0', 0'), gen_0':s4_0(n2097_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n2097₀)
fold(triple(0', 0'), A, gen_0':s4_0(n6349_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n6349₀)

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

No more defined symbols left to analyse.

(33) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
foldC(triple(0', 0'), gen_0':s4_0(n4174_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n4174₀)

(34) BOUNDS(n^1, INF)

(35) Obligation:

Innermost TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(b, c), C) → triple(b, s(c))
f'(triple(b, c), B) → f(triple(b, c), A)
f'(triple(b, c), A) → f''(foldB(triple(0', c), b))
f''(triple(b, c)) → foldC(triple(b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Lemmas:
foldC(triple(0', 0'), gen_0':s4_0(n4174_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n4174₀)
foldB(triple(0', 0'), gen_0':s4_0(n2097_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n2097₀)
fold(triple(0', 0'), A, gen_0':s4_0(n6349_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n6349₀)

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

No more defined symbols left to analyse.

(36) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
foldC(triple(0', 0'), gen_0':s4_0(n4174_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n4174₀)

(37) BOUNDS(n^1, INF)

(38) Obligation:

Innermost TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(b, c), C) → triple(b, s(c))
f'(triple(b, c), B) → f(triple(b, c), A)
f'(triple(b, c), A) → f''(foldB(triple(0', c), b))
f''(triple(b, c)) → foldC(triple(b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Lemmas:
foldC(triple(0', 0'), gen_0':s4_0(n4174_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n4174₀)
foldB(triple(0', 0'), gen_0':s4_0(n2097_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n2097₀)

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

No more defined symbols left to analyse.

(39) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
foldC(triple(0', 0'), gen_0':s4_0(n4174_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n4174₀)

(40) BOUNDS(n^1, INF)

(41) Obligation:

Innermost TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(b, c), C) → triple(b, s(c))
f'(triple(b, c), B) → f(triple(b, c), A)
f'(triple(b, c), A) → f''(foldB(triple(0', c), b))
f''(triple(b, c)) → foldC(triple(b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Lemmas:
foldC(triple(0', 0'), gen_0':s4_0(n143_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n143₀)
foldB(triple(0', 0'), gen_0':s4_0(n2097_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n2097₀)

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

No more defined symbols left to analyse.

(42) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
foldC(triple(0', 0'), gen_0':s4_0(n143_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n143₀)

(43) BOUNDS(n^1, INF)

(44) Obligation:

Innermost TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(b, c), C) → triple(b, s(c))
f'(triple(b, c), B) → f(triple(b, c), A)
f'(triple(b, c), A) → f''(foldB(triple(0', c), b))
f''(triple(b, c)) → foldC(triple(b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Lemmas:
foldC(triple(0', 0'), gen_0':s4_0(n143_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n143₀)

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

No more defined symbols left to analyse.

(45) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
foldC(triple(0', 0'), gen_0':s4_0(n143_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n143₀)

(46) BOUNDS(n^1, INF)